YES 2.97 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((nub :: Eq a => [[a]]  ->  [[a]]) :: Eq a => [[a]]  ->  [[a]])

module List where
  import qualified Maybe
import qualified Prelude

  nub :: Eq a => [a ->  [a]
nub l 
nub' l [] where 
nub' [] _ []
nub' (x : xsls 
 | x `elem` ls = 
nub' xs ls
 | otherwise = 
x : nub' xs (x : ls)


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((nub :: Eq a => [[a]]  ->  [[a]]) :: Eq a => [[a]]  ->  [[a]])

module List where
  import qualified Maybe
import qualified Prelude

  nub :: Eq a => [a ->  [a]
nub l 
nub' l [] where 
nub' [] vw []
nub' (x : xsls 
 | x `elem` ls = 
nub' xs ls
 | otherwise = 
x : nub' xs (x : ls)


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
nub' [] vw = []
nub' (x : xsls
 | x `elem` ls
 = nub' xs ls
 | otherwise
 = x : nub' xs (x : ls)

is transformed to
nub' [] vw = nub'3 [] vw
nub' (x : xsls = nub'2 (x : xsls

nub'1 x xs ls True = nub' xs ls
nub'1 x xs ls False = nub'0 x xs ls otherwise

nub'0 x xs ls True = x : nub' xs (x : ls)

nub'2 (x : xsls = nub'1 x xs ls (x `elem` ls)

nub'3 [] vw = []
nub'3 xz yu = nub'2 xz yu

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ LetRed

mainModule List
  ((nub :: Eq a => [[a]]  ->  [[a]]) :: Eq a => [[a]]  ->  [[a]])

module List where
  import qualified Maybe
import qualified Prelude

  nub :: Eq a => [a ->  [a]
nub l 
nub' l [] where 
nub' [] vw nub'3 [] vw
nub' (x : xsls nub'2 (x : xs) ls
nub'0 x xs ls True x : nub' xs (x : ls)
nub'1 x xs ls True nub' xs ls
nub'1 x xs ls False nub'0 x xs ls otherwise
nub'2 (x : xsls nub'1 x xs ls (x `elem` ls)
nub'3 [] vw []
nub'3 xz yu nub'2 xz yu


module Maybe where
  import qualified List
import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
nub' l []
where 
nub' [] vw = nub'3 [] vw
nub' (x : xsls = nub'2 (x : xsls
nub'0 x xs ls True = x : nub' xs (x : ls)
nub'1 x xs ls True = nub' xs ls
nub'1 x xs ls False = nub'0 x xs ls otherwise
nub'2 (x : xsls = nub'1 x xs ls (x `elem` ls)
nub'3 [] vw = []
nub'3 xz yu = nub'2 xz yu

are unpacked to the following functions on top level
nubNub'3 [] vw = []
nubNub'3 xz yu = nubNub'2 xz yu

nubNub'2 (x : xsls = nubNub'1 x xs ls (x `elem` ls)

nubNub'0 x xs ls True = x : nubNub' xs (x : ls)

nubNub'1 x xs ls True = nubNub' xs ls
nubNub'1 x xs ls False = nubNub'0 x xs ls otherwise

nubNub' [] vw = nubNub'3 [] vw
nubNub' (x : xsls = nubNub'2 (x : xsls



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
HASKELL
              ↳ Narrow

mainModule List
  (nub :: Eq a => [[a]]  ->  [[a]])

module List where
  import qualified Maybe
import qualified Prelude

  nub :: Eq a => [a ->  [a]
nub l nubNub' l []

  
nubNub' [] vw nubNub'3 [] vw
nubNub' (x : xsls nubNub'2 (x : xs) ls

  
nubNub'0 x xs ls True x : nubNub' xs (x : ls)

  
nubNub'1 x xs ls True nubNub' xs ls
nubNub'1 x xs ls False nubNub'0 x xs ls otherwise

  
nubNub'2 (x : xsls nubNub'1 x xs ls (x `elem` ls)

  
nubNub'3 [] vw []
nubNub'3 xz yu nubNub'2 xz yu


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv17300), Succ(yv1451000)) → new_primPlusNat(yv17300, yv1451000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv141100), Succ(yv145100)) → new_primMulNat(yv141100, Succ(yv145100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yv14100), Succ(yv14500)) → new_primEqNat(yv14100, yv14500)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), app(app(app(ty_@3, fg), fh), ga), fb) → new_esEs2(yv1410, yv1450, fg, fh, ga)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, app(ty_Maybe, bbd), bba) → new_esEs1(yv1411, yv1451, bbd)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), app(ty_Maybe, bce), he, bba) → new_esEs1(yv1410, yv1450, bce)
new_esEs3(:(yv1410, yv1411), :(yv1450, yv1451), app(app(ty_Either, bdc), bdd)) → new_esEs(yv1410, yv1450, bdc, bdd)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), app(app(app(ty_@3, bcf), bcg), bch), he, bba) → new_esEs2(yv1410, yv1450, bcf, bcg, bch)
new_esEs3(:(yv1410, yv1411), :(yv1450, yv1451), app(app(ty_@2, bde), bdf)) → new_esEs0(yv1410, yv1450, bde, bdf)
new_esEs3(:(yv1410, yv1411), :(yv1450, yv1451), app(ty_Maybe, bdg)) → new_esEs1(yv1410, yv1450, bdg)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, app(app(ty_@2, bbb), bbc), bba) → new_esEs0(yv1411, yv1451, bbb, bbc)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), app(app(ty_Either, bca), bcb), he, bba) → new_esEs(yv1410, yv1450, bca, bcb)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), df, app(app(app(ty_@3, ed), ee), ef)) → new_esEs2(yv1411, yv1451, ed, ee, ef)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, he, app(app(ty_@2, hh), baa)) → new_esEs0(yv1412, yv1452, hh, baa)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, app(ty_[], bbh), bba) → new_esEs3(yv1411, yv1451, bbh)
new_esEs3(:(yv1410, yv1411), :(yv1450, yv1451), app(ty_[], bec)) → new_esEs3(yv1410, yv1450, bec)
new_esEs1(Just(yv1410), Just(yv1450), app(app(ty_Either, gc), gd)) → new_esEs(yv1410, yv1450, gc, gd)
new_esEs1(Just(yv1410), Just(yv1450), app(ty_[], hc)) → new_esEs3(yv1410, yv1450, hc)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), app(app(ty_@2, bcc), bcd), he, bba) → new_esEs0(yv1410, yv1450, bcc, bcd)
new_esEs(Right(yv1410), Right(yv1450), cc, app(app(ty_@2, cf), cg)) → new_esEs0(yv1410, yv1450, cf, cg)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), df, app(ty_[], eg)) → new_esEs3(yv1411, yv1451, eg)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), app(ty_[], gb), fb) → new_esEs3(yv1410, yv1450, gb)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), app(app(ty_Either, eh), fa), fb) → new_esEs(yv1410, yv1450, eh, fa)
new_esEs1(Just(yv1410), Just(yv1450), app(app(ty_@2, ge), gf)) → new_esEs0(yv1410, yv1450, ge, gf)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), df, app(app(ty_Either, dg), dh)) → new_esEs(yv1411, yv1451, dg, dh)
new_esEs3(:(yv1410, yv1411), :(yv1450, yv1451), bdb) → new_esEs3(yv1411, yv1451, bdb)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, app(app(ty_Either, bag), bah), bba) → new_esEs(yv1411, yv1451, bag, bah)
new_esEs(Left(yv1410), Left(yv1450), app(ty_[], cb), bc) → new_esEs3(yv1410, yv1450, cb)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, he, app(app(ty_Either, hf), hg)) → new_esEs(yv1412, yv1452, hf, hg)
new_esEs(Right(yv1410), Right(yv1450), cc, app(app(ty_Either, cd), ce)) → new_esEs(yv1410, yv1450, cd, ce)
new_esEs(Right(yv1410), Right(yv1450), cc, app(ty_[], de)) → new_esEs3(yv1410, yv1450, de)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, he, app(ty_[], baf)) → new_esEs3(yv1412, yv1452, baf)
new_esEs(Left(yv1410), Left(yv1450), app(app(ty_@2, bd), be), bc) → new_esEs0(yv1410, yv1450, bd, be)
new_esEs3(:(yv1410, yv1411), :(yv1450, yv1451), app(app(app(ty_@3, bdh), bea), beb)) → new_esEs2(yv1410, yv1450, bdh, bea, beb)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, app(app(app(ty_@3, bbe), bbf), bbg), bba) → new_esEs2(yv1411, yv1451, bbe, bbf, bbg)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), app(ty_[], bda), he, bba) → new_esEs3(yv1410, yv1450, bda)
new_esEs(Left(yv1410), Left(yv1450), app(ty_Maybe, bf), bc) → new_esEs1(yv1410, yv1450, bf)
new_esEs1(Just(yv1410), Just(yv1450), app(ty_Maybe, gg)) → new_esEs1(yv1410, yv1450, gg)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), app(app(ty_@2, fc), fd), fb) → new_esEs0(yv1410, yv1450, fc, fd)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, he, app(ty_Maybe, bab)) → new_esEs1(yv1412, yv1452, bab)
new_esEs1(Just(yv1410), Just(yv1450), app(app(app(ty_@3, gh), ha), hb)) → new_esEs2(yv1410, yv1450, gh, ha, hb)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), df, app(ty_Maybe, ec)) → new_esEs1(yv1411, yv1451, ec)
new_esEs(Left(yv1410), Left(yv1450), app(app(app(ty_@3, bg), bh), ca), bc) → new_esEs2(yv1410, yv1450, bg, bh, ca)
new_esEs(Right(yv1410), Right(yv1450), cc, app(app(app(ty_@3, db), dc), dd)) → new_esEs2(yv1410, yv1450, db, dc, dd)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), app(ty_Maybe, ff), fb) → new_esEs1(yv1410, yv1450, ff)
new_esEs0(@2(yv1410, yv1411), @2(yv1450, yv1451), df, app(app(ty_@2, ea), eb)) → new_esEs0(yv1411, yv1451, ea, eb)
new_esEs(Right(yv1410), Right(yv1450), cc, app(ty_Maybe, da)) → new_esEs1(yv1410, yv1450, da)
new_esEs(Left(yv1410), Left(yv1450), app(app(ty_Either, ba), bb), bc) → new_esEs(yv1410, yv1450, ba, bb)
new_esEs2(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hd, he, app(app(app(ty_@3, bac), bad), bae)) → new_esEs2(yv1412, yv1452, bac, bad, bae)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_nubNub'10(yv154, yv155, yv156, yv157, True, yv159, bb) → new_nubNub'(yv155, yv156, yv157, bb)
new_nubNub'1(yv141, yv142, yv143, yv144, yv145, yv146, ba) → new_nubNub'10(yv141, yv142, yv143, yv144, new_esEs4(yv141, yv145, ba), yv146, ba)
new_nubNub'10(yv154, yv155, yv156, yv157, False, :(yv1590, yv1591), bb) → new_nubNub'1(yv154, yv155, yv156, yv157, yv1590, yv1591, bb)
new_nubNub'10(yv154, yv155, yv156, yv157, False, [], bb) → new_nubNub'(yv155, yv154, :(yv156, yv157), bb)
new_nubNub'(:(yv480, yv481), yv49, yv50, bc) → new_nubNub'1(yv480, yv481, yv49, yv50, yv49, yv50, bc)

The TRS R consists of the following rules:

new_esEs23(yv1410, yv1450, ty_Integer) → new_esEs13(yv1410, yv1450)
new_esEs23(yv1410, yv1450, app(app(ty_Either, ee), ef)) → new_esEs12(yv1410, yv1450, ee, ef)
new_esEs25(yv1411, yv1451, app(ty_Maybe, bbd)) → new_esEs14(yv1411, yv1451, bbd)
new_primPlusNat1(Succ(yv17300), Succ(yv1451000)) → Succ(Succ(new_primPlusNat1(yv17300, yv1451000)))
new_primEqInt(Neg(Succ(yv14100)), Pos(yv1450)) → False
new_primEqInt(Pos(Succ(yv14100)), Neg(yv1450)) → False
new_esEs24(yv1412, yv1452, ty_Char) → new_esEs15(yv1412, yv1452)
new_esEs14(Just(yv1410), Just(yv1450), ty_Bool) → new_esEs7(yv1410, yv1450)
new_esEs26(yv1410, yv1450, app(app(ty_Either, bcb), bcc)) → new_esEs12(yv1410, yv1450, bcb, bcc)
new_esEs25(yv1411, yv1451, ty_Ordering) → new_esEs6(yv1411, yv1451)
new_esEs12(Left(yv1410), Left(yv1450), ty_@0, bdd) → new_esEs5(yv1410, yv1450)
new_primEqInt(Neg(Zero), Pos(Succ(yv14500))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yv14500))) → False
new_esEs23(yv1410, yv1450, ty_Double) → new_esEs17(yv1410, yv1450)
new_esEs10(yv1410, yv1450, ty_Int) → new_esEs16(yv1410, yv1450)
new_esEs9(yv1411, yv1451, app(app(ty_@2, bh), ca)) → new_esEs8(yv1411, yv1451, bh, ca)
new_esEs9(yv1411, yv1451, ty_Char) → new_esEs15(yv1411, yv1451)
new_esEs12(Right(yv1410), Right(yv1450), beg, ty_Int) → new_esEs16(yv1410, yv1450)
new_esEs18(:%(yv1410, yv1411), :%(yv1450, yv1451), ec) → new_asAs(new_esEs22(yv1410, yv1450, ec), new_esEs21(yv1411, yv1451, ec))
new_esEs23(yv1410, yv1450, app(ty_Maybe, fa)) → new_esEs14(yv1410, yv1450, fa)
new_esEs20(:(yv1410, yv1411), :(yv1450, yv1451), ed) → new_asAs(new_esEs23(yv1410, yv1450, ed), new_esEs20(yv1411, yv1451, ed))
new_primMulNat0(Zero, Zero) → Zero
new_esEs23(yv1410, yv1450, ty_Ordering) → new_esEs6(yv1410, yv1450)
new_esEs24(yv1412, yv1452, app(app(ty_Either, hf), hg)) → new_esEs12(yv1412, yv1452, hf, hg)
new_esEs24(yv1412, yv1452, ty_Integer) → new_esEs13(yv1412, yv1452)
new_esEs14(Just(yv1410), Just(yv1450), app(ty_[], hb)) → new_esEs20(yv1410, yv1450, hb)
new_esEs4(yv141, yv145, app(ty_Ratio, ec)) → new_esEs18(yv141, yv145, ec)
new_esEs23(yv1410, yv1450, ty_Float) → new_esEs11(yv1410, yv1450)
new_esEs12(Left(yv1410), Left(yv1450), app(ty_Maybe, bea), bdd) → new_esEs14(yv1410, yv1450, bea)
new_esEs9(yv1411, yv1451, app(app(app(ty_@3, cd), ce), cf)) → new_esEs19(yv1411, yv1451, cd, ce, cf)
new_primPlusNat0(Zero, yv145100) → Succ(yv145100)
new_esEs26(yv1410, yv1450, app(ty_Ratio, bcg)) → new_esEs18(yv1410, yv1450, bcg)
new_esEs12(Right(yv1410), Right(yv1450), beg, app(ty_Ratio, bfe)) → new_esEs18(yv1410, yv1450, bfe)
new_esEs25(yv1411, yv1451, app(ty_Ratio, bbe)) → new_esEs18(yv1411, yv1451, bbe)
new_esEs21(yv1411, yv1451, ty_Integer) → new_esEs13(yv1411, yv1451)
new_esEs26(yv1410, yv1450, ty_Char) → new_esEs15(yv1410, yv1450)
new_esEs9(yv1411, yv1451, ty_Int) → new_esEs16(yv1411, yv1451)
new_esEs10(yv1410, yv1450, app(app(ty_Either, da), db)) → new_esEs12(yv1410, yv1450, da, db)
new_sr(Neg(yv14110), Pos(yv14510)) → Neg(new_primMulNat0(yv14110, yv14510))
new_sr(Pos(yv14110), Neg(yv14510)) → Neg(new_primMulNat0(yv14110, yv14510))
new_esEs23(yv1410, yv1450, ty_Char) → new_esEs15(yv1410, yv1450)
new_esEs14(Just(yv1410), Just(yv1450), ty_Float) → new_esEs11(yv1410, yv1450)
new_esEs11(Float(yv1410, yv1411), Float(yv1450, yv1451)) → new_esEs16(new_sr(yv1410, yv1450), new_sr(yv1411, yv1451))
new_esEs24(yv1412, yv1452, app(app(app(ty_@3, bad), bae), baf)) → new_esEs19(yv1412, yv1452, bad, bae, baf)
new_esEs12(Right(yv1410), Left(yv1450), beg, bdd) → False
new_esEs12(Left(yv1410), Right(yv1450), beg, bdd) → False
new_esEs12(Left(yv1410), Left(yv1450), app(app(ty_@2, bdg), bdh), bdd) → new_esEs8(yv1410, yv1450, bdg, bdh)
new_esEs19(@3(yv1410, yv1411, yv1412), @3(yv1450, yv1451, yv1452), hc, hd, he) → new_asAs(new_esEs26(yv1410, yv1450, hc), new_asAs(new_esEs25(yv1411, yv1451, hd), new_esEs24(yv1412, yv1452, he)))
new_esEs4(yv141, yv145, ty_Float) → new_esEs11(yv141, yv145)
new_esEs4(yv141, yv145, app(ty_[], ed)) → new_esEs20(yv141, yv145, ed)
new_esEs9(yv1411, yv1451, app(ty_Ratio, cc)) → new_esEs18(yv1411, yv1451, cc)
new_esEs4(yv141, yv145, app(app(app(ty_@3, hc), hd), he)) → new_esEs19(yv141, yv145, hc, hd, he)
new_esEs12(Right(yv1410), Right(yv1450), beg, app(ty_[], bga)) → new_esEs20(yv1410, yv1450, bga)
new_esEs12(Right(yv1410), Right(yv1450), beg, ty_Bool) → new_esEs7(yv1410, yv1450)
new_esEs9(yv1411, yv1451, ty_Integer) → new_esEs13(yv1411, yv1451)
new_esEs4(yv141, yv145, ty_Integer) → new_esEs13(yv141, yv145)
new_esEs9(yv1411, yv1451, app(ty_Maybe, cb)) → new_esEs14(yv1411, yv1451, cb)
new_esEs12(Left(yv1410), Left(yv1450), app(app(ty_Either, bde), bdf), bdd) → new_esEs12(yv1410, yv1450, bde, bdf)
new_esEs23(yv1410, yv1450, app(ty_[], fg)) → new_esEs20(yv1410, yv1450, fg)
new_esEs26(yv1410, yv1450, ty_@0) → new_esEs5(yv1410, yv1450)
new_primEqNat0(Zero, Succ(yv14500)) → False
new_primEqNat0(Succ(yv14100), Zero) → False
new_esEs10(yv1410, yv1450, ty_Double) → new_esEs17(yv1410, yv1450)
new_esEs24(yv1412, yv1452, app(ty_Maybe, bab)) → new_esEs14(yv1412, yv1452, bab)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs12(Right(yv1410), Right(yv1450), beg, ty_Ordering) → new_esEs6(yv1410, yv1450)
new_esEs23(yv1410, yv1450, app(ty_Ratio, fb)) → new_esEs18(yv1410, yv1450, fb)
new_esEs26(yv1410, yv1450, app(app(ty_@2, bcd), bce)) → new_esEs8(yv1410, yv1450, bcd, bce)
new_esEs24(yv1412, yv1452, ty_Bool) → new_esEs7(yv1412, yv1452)
new_esEs5(@0, @0) → True
new_esEs17(Double(yv1410, yv1411), Double(yv1450, yv1451)) → new_esEs16(new_sr(yv1410, yv1450), new_sr(yv1411, yv1451))
new_esEs7(False, False) → True
new_esEs10(yv1410, yv1450, ty_Bool) → new_esEs7(yv1410, yv1450)
new_esEs12(Left(yv1410), Left(yv1450), app(app(app(ty_@3, bec), bed), bee), bdd) → new_esEs19(yv1410, yv1450, bec, bed, bee)
new_esEs26(yv1410, yv1450, ty_Int) → new_esEs16(yv1410, yv1450)
new_esEs6(GT, LT) → False
new_esEs6(LT, GT) → False
new_esEs9(yv1411, yv1451, ty_@0) → new_esEs5(yv1411, yv1451)
new_esEs25(yv1411, yv1451, ty_Int) → new_esEs16(yv1411, yv1451)
new_esEs25(yv1411, yv1451, ty_Bool) → new_esEs7(yv1411, yv1451)
new_esEs12(Left(yv1410), Left(yv1450), ty_Ordering, bdd) → new_esEs6(yv1410, yv1450)
new_esEs23(yv1410, yv1450, app(app(ty_@2, eg), eh)) → new_esEs8(yv1410, yv1450, eg, eh)
new_esEs9(yv1411, yv1451, ty_Double) → new_esEs17(yv1411, yv1451)
new_esEs20([], [], ed) → True
new_esEs10(yv1410, yv1450, ty_@0) → new_esEs5(yv1410, yv1450)
new_esEs14(Just(yv1410), Just(yv1450), ty_Integer) → new_esEs13(yv1410, yv1450)
new_esEs26(yv1410, yv1450, ty_Double) → new_esEs17(yv1410, yv1450)
new_esEs10(yv1410, yv1450, ty_Float) → new_esEs11(yv1410, yv1450)
new_esEs26(yv1410, yv1450, ty_Bool) → new_esEs7(yv1410, yv1450)
new_esEs12(Right(yv1410), Right(yv1450), beg, ty_Char) → new_esEs15(yv1410, yv1450)
new_esEs25(yv1411, yv1451, ty_@0) → new_esEs5(yv1411, yv1451)
new_esEs25(yv1411, yv1451, ty_Double) → new_esEs17(yv1411, yv1451)
new_sr(Neg(yv14110), Neg(yv14510)) → Pos(new_primMulNat0(yv14110, yv14510))
new_esEs9(yv1411, yv1451, app(app(ty_Either, bf), bg)) → new_esEs12(yv1411, yv1451, bf, bg)
new_esEs14(Nothing, Nothing, fh) → True
new_sr(Pos(yv14110), Pos(yv14510)) → Pos(new_primMulNat0(yv14110, yv14510))
new_asAs(False, yv172) → False
new_esEs9(yv1411, yv1451, ty_Bool) → new_esEs7(yv1411, yv1451)
new_esEs25(yv1411, yv1451, app(ty_[], bca)) → new_esEs20(yv1411, yv1451, bca)
new_esEs24(yv1412, yv1452, ty_Int) → new_esEs16(yv1412, yv1452)
new_primEqNat0(Zero, Zero) → True
new_esEs26(yv1410, yv1450, ty_Ordering) → new_esEs6(yv1410, yv1450)
new_primMulNat0(Succ(yv141100), Zero) → Zero
new_primMulNat0(Zero, Succ(yv145100)) → Zero
new_esEs12(Left(yv1410), Left(yv1450), ty_Integer, bdd) → new_esEs13(yv1410, yv1450)
new_esEs26(yv1410, yv1450, ty_Integer) → new_esEs13(yv1410, yv1450)
new_esEs12(Right(yv1410), Right(yv1450), beg, ty_Float) → new_esEs11(yv1410, yv1450)
new_esEs10(yv1410, yv1450, app(app(ty_@2, dc), dd)) → new_esEs8(yv1410, yv1450, dc, dd)
new_esEs21(yv1411, yv1451, ty_Int) → new_esEs16(yv1411, yv1451)
new_esEs14(Just(yv1410), Just(yv1450), ty_Int) → new_esEs16(yv1410, yv1450)
new_esEs4(yv141, yv145, ty_Bool) → new_esEs7(yv141, yv145)
new_esEs12(Right(yv1410), Right(yv1450), beg, ty_Integer) → new_esEs13(yv1410, yv1450)
new_esEs24(yv1412, yv1452, ty_@0) → new_esEs5(yv1412, yv1452)
new_esEs10(yv1410, yv1450, app(ty_Ratio, df)) → new_esEs18(yv1410, yv1450, df)
new_esEs4(yv141, yv145, ty_Int) → new_esEs16(yv141, yv145)
new_esEs24(yv1412, yv1452, ty_Float) → new_esEs11(yv1412, yv1452)
new_esEs23(yv1410, yv1450, ty_Bool) → new_esEs7(yv1410, yv1450)
new_esEs25(yv1411, yv1451, ty_Integer) → new_esEs13(yv1411, yv1451)
new_esEs12(Left(yv1410), Left(yv1450), app(ty_[], bef), bdd) → new_esEs20(yv1410, yv1450, bef)
new_esEs15(Char(yv1410), Char(yv1450)) → new_primEqNat0(yv1410, yv1450)
new_esEs12(Left(yv1410), Left(yv1450), ty_Float, bdd) → new_esEs11(yv1410, yv1450)
new_esEs10(yv1410, yv1450, app(ty_Maybe, de)) → new_esEs14(yv1410, yv1450, de)
new_esEs14(Just(yv1410), Just(yv1450), app(ty_Maybe, ge)) → new_esEs14(yv1410, yv1450, ge)
new_esEs14(Just(yv1410), Just(yv1450), app(ty_Ratio, gf)) → new_esEs18(yv1410, yv1450, gf)
new_esEs12(Left(yv1410), Left(yv1450), ty_Int, bdd) → new_esEs16(yv1410, yv1450)
new_esEs14(Just(yv1410), Just(yv1450), app(app(ty_Either, ga), gb)) → new_esEs12(yv1410, yv1450, ga, gb)
new_primPlusNat0(Succ(yv1730), yv145100) → Succ(Succ(new_primPlusNat1(yv1730, yv145100)))
new_esEs12(Left(yv1410), Left(yv1450), ty_Double, bdd) → new_esEs17(yv1410, yv1450)
new_esEs23(yv1410, yv1450, ty_Int) → new_esEs16(yv1410, yv1450)
new_esEs26(yv1410, yv1450, ty_Float) → new_esEs11(yv1410, yv1450)
new_esEs24(yv1412, yv1452, ty_Double) → new_esEs17(yv1412, yv1452)
new_esEs13(Integer(yv1410), Integer(yv1450)) → new_primEqInt(yv1410, yv1450)
new_esEs4(yv141, yv145, app(app(ty_Either, beg), bdd)) → new_esEs12(yv141, yv145, beg, bdd)
new_esEs12(Left(yv1410), Left(yv1450), app(ty_Ratio, beb), bdd) → new_esEs18(yv1410, yv1450, beb)
new_esEs14(Nothing, Just(yv1450), fh) → False
new_esEs14(Just(yv1410), Nothing, fh) → False
new_esEs12(Right(yv1410), Right(yv1450), beg, app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs19(yv1410, yv1450, bff, bfg, bfh)
new_primEqInt(Neg(Succ(yv14100)), Neg(Succ(yv14500))) → new_primEqNat0(yv14100, yv14500)
new_esEs25(yv1411, yv1451, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs19(yv1411, yv1451, bbf, bbg, bbh)
new_esEs4(yv141, yv145, ty_Double) → new_esEs17(yv141, yv145)
new_esEs25(yv1411, yv1451, app(app(ty_@2, bbb), bbc)) → new_esEs8(yv1411, yv1451, bbb, bbc)
new_esEs8(@2(yv1410, yv1411), @2(yv1450, yv1451), bd, be) → new_asAs(new_esEs10(yv1410, yv1450, bd), new_esEs9(yv1411, yv1451, be))
new_primPlusNat1(Zero, Succ(yv1451000)) → Succ(yv1451000)
new_primPlusNat1(Succ(yv17300), Zero) → Succ(yv17300)
new_esEs6(GT, GT) → True
new_esEs25(yv1411, yv1451, ty_Char) → new_esEs15(yv1411, yv1451)
new_esEs6(GT, EQ) → False
new_esEs6(EQ, GT) → False
new_esEs7(True, True) → True
new_esEs12(Right(yv1410), Right(yv1450), beg, ty_Double) → new_esEs17(yv1410, yv1450)
new_esEs16(yv141, yv145) → new_primEqInt(yv141, yv145)
new_esEs6(EQ, EQ) → True
new_esEs9(yv1411, yv1451, ty_Float) → new_esEs11(yv1411, yv1451)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(yv1410, yv1450, app(app(app(ty_@3, fc), fd), ff)) → new_esEs19(yv1410, yv1450, fc, fd, ff)
new_esEs12(Right(yv1410), Right(yv1450), beg, app(ty_Maybe, bfd)) → new_esEs14(yv1410, yv1450, bfd)
new_esEs12(Right(yv1410), Right(yv1450), beg, app(app(ty_Either, beh), bfa)) → new_esEs12(yv1410, yv1450, beh, bfa)
new_esEs25(yv1411, yv1451, app(app(ty_Either, bah), bba)) → new_esEs12(yv1411, yv1451, bah, bba)
new_esEs26(yv1410, yv1450, app(ty_Maybe, bcf)) → new_esEs14(yv1410, yv1450, bcf)
new_esEs4(yv141, yv145, app(app(ty_@2, bd), be)) → new_esEs8(yv141, yv145, bd, be)
new_esEs20(:(yv1410, yv1411), [], ed) → False
new_esEs20([], :(yv1450, yv1451), ed) → False
new_esEs4(yv141, yv145, ty_Char) → new_esEs15(yv141, yv145)
new_primEqInt(Neg(Zero), Neg(Succ(yv14500))) → False
new_primEqInt(Neg(Succ(yv14100)), Neg(Zero)) → False
new_esEs10(yv1410, yv1450, ty_Integer) → new_esEs13(yv1410, yv1450)
new_esEs7(False, True) → False
new_esEs7(True, False) → False
new_esEs14(Just(yv1410), Just(yv1450), ty_@0) → new_esEs5(yv1410, yv1450)
new_esEs12(Left(yv1410), Left(yv1450), ty_Bool, bdd) → new_esEs7(yv1410, yv1450)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs10(yv1410, yv1450, app(app(app(ty_@3, dg), dh), ea)) → new_esEs19(yv1410, yv1450, dg, dh, ea)
new_esEs12(Left(yv1410), Left(yv1450), ty_Char, bdd) → new_esEs15(yv1410, yv1450)
new_asAs(True, yv172) → yv172
new_esEs10(yv1410, yv1450, ty_Ordering) → new_esEs6(yv1410, yv1450)
new_primMulNat0(Succ(yv141100), Succ(yv145100)) → new_primPlusNat0(new_primMulNat0(yv141100, Succ(yv145100)), yv145100)
new_esEs12(Right(yv1410), Right(yv1450), beg, app(app(ty_@2, bfb), bfc)) → new_esEs8(yv1410, yv1450, bfb, bfc)
new_esEs25(yv1411, yv1451, ty_Float) → new_esEs11(yv1411, yv1451)
new_esEs24(yv1412, yv1452, ty_Ordering) → new_esEs6(yv1412, yv1452)
new_primEqInt(Pos(Succ(yv14100)), Pos(Succ(yv14500))) → new_primEqNat0(yv14100, yv14500)
new_esEs26(yv1410, yv1450, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs19(yv1410, yv1450, bch, bda, bdb)
new_esEs6(EQ, LT) → False
new_esEs6(LT, EQ) → False
new_esEs24(yv1412, yv1452, app(app(ty_@2, hh), baa)) → new_esEs8(yv1412, yv1452, hh, baa)
new_esEs9(yv1411, yv1451, app(ty_[], cg)) → new_esEs20(yv1411, yv1451, cg)
new_primEqNat0(Succ(yv14100), Succ(yv14500)) → new_primEqNat0(yv14100, yv14500)
new_esEs24(yv1412, yv1452, app(ty_[], bag)) → new_esEs20(yv1412, yv1452, bag)
new_esEs24(yv1412, yv1452, app(ty_Ratio, bac)) → new_esEs18(yv1412, yv1452, bac)
new_esEs4(yv141, yv145, app(ty_Maybe, fh)) → new_esEs14(yv141, yv145, fh)
new_esEs9(yv1411, yv1451, ty_Ordering) → new_esEs6(yv1411, yv1451)
new_esEs4(yv141, yv145, ty_@0) → new_esEs5(yv141, yv145)
new_esEs12(Right(yv1410), Right(yv1450), beg, ty_@0) → new_esEs5(yv1410, yv1450)
new_esEs14(Just(yv1410), Just(yv1450), ty_Double) → new_esEs17(yv1410, yv1450)
new_esEs4(yv141, yv145, ty_Ordering) → new_esEs6(yv141, yv145)
new_esEs14(Just(yv1410), Just(yv1450), app(app(ty_@2, gc), gd)) → new_esEs8(yv1410, yv1450, gc, gd)
new_esEs14(Just(yv1410), Just(yv1450), app(app(app(ty_@3, gg), gh), ha)) → new_esEs19(yv1410, yv1450, gg, gh, ha)
new_esEs14(Just(yv1410), Just(yv1450), ty_Ordering) → new_esEs6(yv1410, yv1450)
new_esEs14(Just(yv1410), Just(yv1450), ty_Char) → new_esEs15(yv1410, yv1450)
new_primEqInt(Pos(Zero), Pos(Succ(yv14500))) → False
new_primEqInt(Pos(Succ(yv14100)), Pos(Zero)) → False
new_esEs26(yv1410, yv1450, app(ty_[], bdc)) → new_esEs20(yv1410, yv1450, bdc)
new_esEs10(yv1410, yv1450, ty_Char) → new_esEs15(yv1410, yv1450)
new_esEs22(yv1410, yv1450, ty_Integer) → new_esEs13(yv1410, yv1450)
new_esEs6(LT, LT) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs23(yv1410, yv1450, ty_@0) → new_esEs5(yv1410, yv1450)
new_esEs10(yv1410, yv1450, app(ty_[], eb)) → new_esEs20(yv1410, yv1450, eb)
new_esEs22(yv1410, yv1450, ty_Int) → new_esEs16(yv1410, yv1450)

The set Q consists of the following terms:

new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs26(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Integer)
new_esEs5(@0, @0)
new_esEs24(x0, x1, ty_Int)
new_esEs12(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs12(Left(x0), Left(x1), ty_Integer, x2)
new_esEs23(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs12(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs20([], :(x0, x1), x2)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs20([], [], x0)
new_esEs6(GT, LT)
new_esEs6(LT, GT)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs9(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs12(Left(x0), Left(x1), ty_@0, x2)
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs10(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Int)
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs23(x0, x1, ty_Bool)
new_esEs14(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs7(False, False)
new_esEs14(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs6(LT, EQ)
new_esEs6(EQ, LT)
new_esEs4(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(Right(x0), Right(x1), x2, ty_Int)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs4(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Ordering)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs21(x0, x1, ty_Int)
new_sr(Neg(x0), Neg(x1))
new_esEs6(EQ, EQ)
new_esEs14(Just(x0), Just(x1), ty_Char)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs14(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs12(Right(x0), Right(x1), x2, ty_@0)
new_primEqNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(LT, LT)
new_esEs12(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs12(Left(x0), Left(x1), ty_Float, x2)
new_esEs14(Nothing, Nothing, x0)
new_esEs14(Nothing, Just(x0), x1)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, ty_@0)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs12(Right(x0), Right(x1), x2, ty_Integer)
new_esEs12(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs10(x0, x1, ty_Double)
new_esEs7(True, False)
new_esEs7(False, True)
new_esEs12(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_Float)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(Left(x0), Right(x1), x2, x3)
new_esEs12(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, ty_Char)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Int)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs4(x0, x1, ty_Bool)
new_esEs10(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(x0, x1, ty_Float)
new_esEs12(Right(x0), Right(x1), x2, ty_Double)
new_esEs12(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Double(x0, x1), Double(x2, x3))
new_esEs12(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs12(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_asAs(True, x0)
new_esEs26(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Float)
new_asAs(False, x0)
new_esEs12(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs24(x0, x1, ty_Double)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_primPlusNat1(Zero, Succ(x0))
new_esEs26(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(GT, GT)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Zero, Zero)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Bool)
new_esEs6(EQ, GT)
new_esEs6(GT, EQ)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Char)
new_esEs14(Just(x0), Just(x1), ty_Integer)
new_esEs10(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs7(True, True)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs15(Char(x0), Char(x1))
new_esEs9(x0, x1, ty_Char)
new_esEs14(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs12(Left(x0), Left(x1), ty_Int, x2)
new_esEs14(Just(x0), Just(x1), ty_Float)
new_esEs4(x0, x1, ty_Char)
new_esEs12(Right(x0), Right(x1), x2, ty_Char)
new_esEs21(x0, x1, ty_Integer)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs20(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs12(Right(x0), Right(x1), x2, ty_Float)
new_esEs19(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs12(Right(x0), Right(x1), x2, ty_Bool)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs14(Just(x0), Just(x1), ty_Bool)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(Left(x0), Left(x1), ty_Double, x2)
new_esEs14(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs9(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs12(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs12(Left(x0), Left(x1), ty_Char, x2)
new_esEs25(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Float)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, ty_Bool)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Float)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Int)
new_primPlusNat1(Zero, Zero)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_@0)
new_esEs14(Just(x0), Just(x1), ty_Double)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Succ(x0), Zero)
new_esEs12(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs8(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs16(x0, x1)
new_esEs12(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs12(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs20(:(x0, x1), [], x2)
new_esEs14(Just(x0), Nothing, x1)
new_esEs14(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs12(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Ordering)
new_esEs14(Just(x0), Just(x1), ty_@0)
new_esEs25(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Integer)
new_esEs14(Just(x0), Just(x1), app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs13(Integer(x0), Integer(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs26(x0, x1, ty_Integer)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: